/*
 * Alloy Analyzer
 * Copyright (c) 2002 Massachusetts Institute of Technology
 *
 * The Alloy Analyzer is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * The Alloy Analyzer is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with the Alloy Analyzer; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place, Suite 330, Boston, MA  02111-1307  USA
 */

package alloy.transform;

import java.util.ArrayList;
import java.util.Collections;
import java.util.HashMap;
import java.util.Iterator;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.TreeMap;
import java.util.TreeSet;

import alloy.ast.ASTDepthFirstReplacer;
import alloy.ast.BinaryExpr;
import alloy.ast.BinaryExprOp;
import alloy.ast.BinaryFormula;
import alloy.ast.CompOp;
import alloy.ast.ComprehensionExpr;
import alloy.ast.IfThenElseExpr;
import alloy.ast.IfThenElseIntExpr;
import alloy.ast.Decl;
import alloy.ast.Decls;
import alloy.ast.ElemFormula;
import alloy.ast.Expr;
import alloy.ast.Formula;
import alloy.ast.FormulaSeq;
import alloy.ast.Formulas;
import alloy.ast.Id;
import alloy.ast.ImplicationFormula;
import alloy.ast.LeafId;
import alloy.ast.LogicOp;
import alloy.ast.MultiplicityExpr;
import alloy.ast.MultiplicityFormula;
import alloy.ast.NegFormula;
import alloy.ast.Node;
import alloy.ast.Qualifiers;
import alloy.ast.QuantifiedFormula;
import alloy.ast.Quantifier;
import alloy.ast.Variable;
import alloy.ast.VariableExpr;
import alloy.ast.Variables;
import alloy.semantic.LocalScope;
import alloy.type.UnionType;
import alloy.util.AlloyConstants;
import alloy.util.Dbg;
import alloy.util.Namer;
import alloy.util.Params;

/**
   <p>Performs skolemization on a formula.

   <p>This visitor assumes that
   all desugarings necessary before translation have been completed,
   and should be applied to a formula associated with a command.
*/

public final class SkolemizationVisitor extends ASTDepthFirstReplacer
    implements AlloyConstants {

    /** leaf id mapping for skolem functions */
    public static LeafIdMap skolemLeafIdMap; // DFR: gets collected

    /**
     * Leaf ids of skolem constants.  Used to test whether a leaf
     * is a skolem constant.
     */
    public static Set /* of LeafId */ skolemLeafIds; // DFR: not collected

    /**
     * The type of each skolem constant: map from String skolem name
     * to UnionType type of the skolem constant with that name.
     * Skolem constants have globally unique names.
     */
    public static Map /* String -> UnionType */ skolemTypes; // DFR: not collected

    /** a mapping from LeafIds of variables that have
        been skolemized to the expressions which should replace
        them in the formula.
    */
    private Map _idToSkolemExpr = new HashMap(); // LeafId -> Expr

    /** a list of {@link alloy.ast.VariableExpr} nodes corresponding
        to the currently scoped universally quantified variables.  used
        to create skolem exprs for nested existential quantifiers. */
    private List _univVarExprs = new ArrayList(); // VariableExpr

    /**
       a map from the variable expressions in {@link #_univVarExprs} to
       the set for each variable seen in its declaration */
    private Map _varExprToSet = new HashMap(); // VariableExpr -> Expr

    /** map from leaf ids to mult exprs */
    private Map _leafIdToMult;

    /** true if skolemization should still be attempted */
    private boolean _doSkolem = true;

    /** counter for creating unique identifiers for skolem constants. */
    private int _counter;

    /** 
     * Maximum nesting depth of universal quantifiers from which to skolemize.
     * Two is the default value.  User-setable in Params.glob.getIntParam("MAIN", "skoldepth").
     */
    public static int maxSkolDepth = 2;


    /** Map from {@link FormulaSeq} skolem constraints to {@link QuantifiedFormula}
        whose body should include constraints, or <code>null</code> if constraints
        should be attached to outermost formula */
    private Map _constraintsToFormula = new TreeMap(); // Map[FormulaSeq -> QuantifiedFormula]

    /** current innermost universally quantified formula, <code>null</code> if no such
        formula exists */
    private QuantifiedFormula _enclosingQuantForm = null;

    /**
     * A generator of unique names, used to get unique skolem constant names.
     */
    private Namer _skolemNamer = new Namer();

    //////////////
    // Methods //
    ////////////

    /** no instances from outside */
    private SkolemizationVisitor(Map leafIdToMult_) {
        _leafIdToMult = leafIdToMult_;
    }

    /**
     * Gather existing identifier names to avoid conflicting with them when
     * we create skolem constant names.
     */
    private void _initSkolemNamer(Formula formula_) {
        GatherNamesVisitor gv = new GatherNamesVisitor();
        formula_.applyVisitor(gv);
        //System.out.println("names to avoid: " + gv.getNames());
        for (Iterator nameIter = gv.getNames().iterator(); nameIter.hasNext();) {
            String name = (String)nameIter.next();
            _skolemNamer.addNameToAvoid(name);
        }
    }

    /**
     * Skolemizes  a given Alloy formula.  Sets {@link #skolemLeafIdMap} and
     * {@link #skolemLeafIds}.
     *
     * @return a version of formula_ with existential quantifiers
     *   skolemized
     */
    public static Formula skolemize(Formula formula_, Map leafIdToMult_) {

        clearState();

        // first, NNF the formula
        // NOTE: fix NNFVisitor so it takes better advantage of maxSkolDepth
        formula_ = (Formula) formula_.applyReturnVisitor(new NNFVisitor(maxSkolDepth > 0));

        // then, skolemize
        SkolemizationVisitor sv = new SkolemizationVisitor(leafIdToMult_);
        sv._initSkolemNamer(formula_);
        formula_ = (Formula)formula_.applyReturnVisitor(sv);

        skolemLeafIds = Collections.unmodifiableSet(skolemLeafIds);

        // finally, insert skolem function constraints in appropriate places
        return _insertConstraints(sv._constraintsToFormula, formula_);
    }

	public static void clearState() {
		skolemLeafIdMap = new LeafIdMap(null);
        skolemLeafIds = new TreeSet();
        skolemTypes = new HashMap();
	}

    private static Formula _insertConstraints(Map constraintsToFormula_, Formula formula_) {
        Iterator entryIter = constraintsToFormula_.entrySet().iterator();
        while (entryIter.hasNext()) {
            Map.Entry entry = (Map.Entry)entryIter.next();
            FormulaSeq constraints = (FormulaSeq)entry.getKey();
            QuantifiedFormula insertionForm = (QuantifiedFormula)entry.getValue();
            if (insertionForm == null) { // insert at top-level
                if (formula_ instanceof FormulaSeq) {
                    ((FormulaSeq)formula_).getFormulas().addFormula(constraints);
                } else {
                    formula_ = new BinaryFormula(formula_, LogicOp.AND, constraints);
                }
            } else {
                Formula f = insertionForm.getFormula();
                if (f instanceof FormulaSeq) {
                    ((FormulaSeq)f).getFormulas().addFormula(constraints);
                } else {
                    Formulas forms = new Formulas();
                    forms.addFormula(f);
                    forms.addFormula(constraints);
                    insertionForm.setFormula(new FormulaSeq(forms));
                }
            }
        }
        return formula_;
    }

    public Object visit(QuantifiedFormula quantFormula_) {
        //System.out.println("skolemizing " + quantFormula_.nodeString());
        Formula ret = quantFormula_;
        // visit decls
        quantFormula_.setDecls((Decls) quantFormula_.getDecls().applyReturnVisitor(this));
        
        if (_doSkolem) {
            Quantifier quant = quantFormula_.getQuantifier();

            if (quant.equals(Quantifier.ALL)) {
                // update enclosing univ. quant. form
                QuantifiedFormula oldEnclosingForm = _enclosingQuantForm;
                _enclosingQuantForm = quantFormula_;
                if (maxSkolDepth > 0) {
                    // save current list and map of universally quantified vars
                    List oldUnivVarExprs = new ArrayList(_univVarExprs);
                    Map oldVarExprToSet = new HashMap(_varExprToSet);
                    // add all variables in current formula to list
                    boolean higherOrder = _addUnivVars(quantFormula_);
                    if (higherOrder) {
                        // don't skolemize within higher-order quantifiers
                        boolean oldSkolem = _doSkolem;
                        _doSkolem = false;
                        // visit body
                        quantFormula_.setFormula((Formula) quantFormula_.getFormula().applyReturnVisitor(this));
                        _doSkolem = oldSkolem;
                    } else {
                        // visit body
                        quantFormula_.setFormula((Formula) quantFormula_.getFormula().applyReturnVisitor(this));
                    }
                    // restore original univ var expr list
                    _univVarExprs = oldUnivVarExprs;
                    _varExprToSet = oldVarExprToSet;
                } else {
                    boolean oldSkolem = _doSkolem;
                    _doSkolem = false;
                    // visit body
                    quantFormula_.setFormula((Formula) quantFormula_.getFormula().applyReturnVisitor(this));
                    _doSkolem = oldSkolem;
                }
                _enclosingQuantForm = oldEnclosingForm;
            } else if (quant.equals(Quantifier.SOME)) {
                // update skolem expr mapping
                FormulaSeq[] skolemConstraints = _createSkolemExprs(quantFormula_);
                // map constraints to current enclosing universally quantified
                // formula
                _constraintsToFormula.put(skolemConstraints[0],
                        _enclosingQuantForm);
                // visit body
                Formula body = quantFormula_.getFormula();
                body = (Formula) body.applyReturnVisitor(this);
                // get rid of existential quantifier and append skolem
                // constraints
                // conjoin multiplicity constraints
                Formulas f = new Formulas();
                f.addFormula(body);
                f.addFormula(skolemConstraints[1]);
                body = new FormulaSeq(f);
                body.annotateTransformReplacing(
                        "existential quantifier skolemized", quantFormula_);
                ret = body;
            } else {
                Dbg.fatal("unknown quantified formula type");
            }
        } else {
            // just visit body
            quantFormula_.setFormula((Formula) quantFormula_.getFormula().applyReturnVisitor(this));
        }
        return ret;
    }

    public Object visit(ComprehensionExpr compExpr_) {
        // don't skolemize within comprehension expressions
        boolean oldSkolem = _doSkolem;
        _doSkolem = false;
        Object ret = visit((Node) compExpr_);
        _doSkolem = oldSkolem;
        return ret;
    }

    public Object visit(IfThenElseExpr ifThenElse) {
        // don't skolemize within if-then-else,
        // to be safe
        // there may be a way to skolemize some formulas
        // under the if, being conservative for now
        boolean oldSkolem = _doSkolem;
        _doSkolem = false;
        Object ret = visit((Node) ifThenElse);
        _doSkolem = oldSkolem;
        return ret;
    }

    public Object visit(IfThenElseIntExpr ifThenElseInt) {
        // don't skolemize within if-then-else,
        // to be safe
        // there may be a way to skolemize some formulas
        // under the if, being conservative for now
        boolean oldSkolem = _doSkolem;
        _doSkolem = false;
        Object ret = visit((Node) ifThenElseInt);
        _doSkolem = oldSkolem;
        return ret;
    }
    
    public Object visit(NegFormula negFormula_) {
        // don't skolemize within negations
        // (assumes NNFVisitor has been run)
        boolean oldSkolem = _doSkolem;
        _doSkolem = false;
        Object ret = visit((Node) negFormula_);
        _doSkolem = oldSkolem;
        return ret;
    }

    public Object visit(ImplicationFormula impFormula_) {
        // given A implies B else C, don't skolemize within A
        // since this is logically equivalent to
        // (!A || B) && (A || C) and A is negated
        boolean oldSkolem = _doSkolem;
        _doSkolem = false;
        impFormula_.getIfFormula().applyReturnVisitor(this);
        _doSkolem = oldSkolem;
        // we can still skolemize in then and else formulas
        Formula origThenFormula = impFormula_.getThenFormula();
        Formula newThenFormula = (Formula)origThenFormula.applyReturnVisitor(this);
        if (origThenFormula != newThenFormula) {
            impFormula_.setThenFormula(newThenFormula);
        }
        Formula origElseFormula = impFormula_.getElseFormula();
        Formula newElseFormula = (Formula)origElseFormula.applyReturnVisitor(this);
        if (origElseFormula != newElseFormula) {
            impFormula_.setElseFormula(newElseFormula);
        }
        return impFormula_;
    }
    
    public Object visit(VariableExpr varExpr_) {
        //System.out.println(varExpr_.fullString());
        // see if variable is existentially quantified
        LeafId id = varExpr_.getLeafId();
        if (_idToSkolemExpr.containsKey(id)) {
            // replace with skolem expr
            Expr replacement = (Expr) ((Expr) _idToSkolemExpr.get(id)).copy();
            replacement.annotateTransformReplacing("replaced with skolem constant", varExpr_);
            return replacement;
        }
        return varExpr_;
    }

    /** update the universally quantified variable list and
        variable to set maps with the variables from a quantified formula.
        @param quantFormula_ the quantified formula, quantifier must be "all"
        @return <code>true</code> if some variable is quantified higher-order
        (in which case no skolemization can be done inside the formula), <code>false</code>
        otherwise
    */
    private boolean _addUnivVars(QuantifiedFormula quantFormula_) {
        LocalScope localScope = quantFormula_.getLocalScope();
        LeafIdMap leafIdMap = quantFormula_.getLeafIdMap();
        Iterator declIter = quantFormula_.getDecls().getDeclIter();
        while (declIter.hasNext()) {
            Decl decl = (Decl)declIter.next();
            // if declaration is higher order, then return
            if (decl.isHigherOrder()) return true;
            // keep expr for set membership
            Expr setExpr = decl.getExpr().toExpr();
            // iterate through variables
            Iterator varIter = decl.getVariables().getVariableIter();
            while (varIter.hasNext()) {
                String varName = ((Variable)varIter.next()).toString();
                VariableExpr varExpr = new VariableExpr(new Variable(new Id(varName)));
                UnionType exprType = localScope.lookupType(varName);
                varExpr.setType(exprType);
                varExpr.setLeafId(leafIdMap.lookupLeafId(varName));
                varExpr.isQuantified = true;
                _univVarExprs.add(varExpr);
                if (_univVarExprs.size() > maxSkolDepth) return true;
                _varExprToSet.put(varExpr, setExpr.copy());
            }
        }
        return false;
    }


    /** create skolem functions for all variables
        quantified in a formula and also expressions
        which can be used to replace the variables in
        the body of the formula */
    private FormulaSeq[] _createSkolemExprs(QuantifiedFormula quantFormula_) {
        LocalScope localScope = quantFormula_.getLocalScope();
        LeafIdMap leafIdMap = quantFormula_.getLeafIdMap();
        Formulas setMembConstraints = new Formulas();
        Formulas multConstraints = new Formulas();
        // construct prefix for types of skolem functions
        // and prefix for skolem expressions
        Expr skolemSetPrefix = _createSkolemSetPrefix();
        UnionType skolemTypePrefix = (skolemSetPrefix == null) ? UnionType.empty(1) : skolemSetPrefix.getType();

        // now construct skolem functions and skolem exprs
        Iterator declIter = quantFormula_.getDecls().getDeclIter();
        while (declIter.hasNext()) {
            Decl decl = (Decl) declIter.next();
            // visit mult expr
            decl.setExpr((MultiplicityExpr)decl.getExpr().applyReturnVisitor(this));
            MultiplicityExpr multExpr = decl.getExpr();
            Iterator varIter = decl.getVariables().getVariableIter();
            while (varIter.hasNext()) {
                Variable var = (Variable) varIter.next();
                String varName = var.nodeString();
                String varBaseName = var.origName!=null ? var.origName : varName;
                UnionType varType = localScope.lookupType(varName);
                LeafId varId = leafIdMap.lookupLeafId(varName);
                Formula[] constraints = _skolemizeVar(var, varBaseName, varType, varId, multExpr, skolemSetPrefix);
                setMembConstraints.addFormula(constraints[0]);
                if (constraints[1] != null) multConstraints.addFormula(constraints[1]);
            }
        }
        setMembConstraints.applyReturnVisitor(new DesugarQuantifiersVisitor());
        multConstraints.applyReturnVisitor(new DesugarQuantifiersVisitor());
        FormulaSeq[] ret = new FormulaSeq[2];
        FormulaSeq seq1 = new FormulaSeq(setMembConstraints);
        seq1.annotate("constraints from skolemization");
        ret[0] = seq1;
        FormulaSeq seq2 = new FormulaSeq(multConstraints);
        seq2.annotate("constraints from skolemization");
        ret[1] = seq2;
        return ret;
    }

    /**
       skolemizes a variable.
       @param name_ name of variable to be skolemized
       @param type_ variable's type
       @param id_ variable's leaf id
       @param multExpr_ multiplicity expr on RHS of variable declaration
       @param setPrefix_ set prefix expression representing universally quantified variables in scope
       @return constraints on the new skolem function, which should be conjoined to the original
       formula appropriately
    */
    private Formula[] _skolemizeVar(Variable var_, String name_, UnionType type_, LeafId id_,
                                    MultiplicityExpr multExpr_, Expr setPrefix_) {
        // create new variable for skolem function
        // here we must append the name separator and another integer
        // to ensure the name of the skolem constant is unique.  even
        // though we already renamed all quantified variables in the
        // original spec to have unique names, there still may be duplicate
        // names in the final formula if a function is invoked multiple
        // times

        // check if name already skolemized, and only add extra number if necessary
        // NOTE: disabled because it breaks SolutionDataImpl's detection of skolem
        // constants, needs to be fixed
        //         Variable skolemVar = null;
        //         if (skolemLeafIdMap.lookupLeafId(name_) != null) {
        String uniqueVarName = _skolemNamer.getUniqueName((var_.paragraphName != null ?
							   var_.paragraphName.getId().toString() + "_" : "") + name_);
	/**
	System.out.println("base " + (var_.paragraphName != null ?
				      var_.paragraphName.getId().toString() + "_" : "") + name_ +
			   " -> " + uniqueVarName);
	**/
        Variable skolemVar = new Variable(new Id(uniqueVarName));
        //Variable skolemVar = new Variable(new Id(name_ + NAME_SEPARATOR + _counter++));

        //         } else {
        //             skolemVar = new Variable(new Id(name_));
        //         }


        // create skolem function
        VariableExpr skolemFunction = new VariableExpr((Variable) skolemVar.copy());
        skolemFunction.setType(setPrefix_ == null ? type_ : setPrefix_.getType().product(type_));
	skolemTypes.put(uniqueVarName, skolemFunction.getType());

        // add to global list of skolem constants
        // NOTE: okay to comment out, not used (i think)
        //skolemConstants.add(skolemFunction);


        // skolem function gets new leaf id
        LeafId skolemId = new LeafId();
        skolemFunction.setLeafId(skolemId);
        skolemLeafIdMap.put(skolemVar.nodeString(), skolemId);
        skolemLeafIds.add(skolemId);

        // create skolem expr, which replaces previous occurrences of quantified variable
        Expr skolemExpr = _createSkolemExpr(skolemFunction);
        Dbg.chk(skolemExpr.getType().equals(type_));

        // map original var's id to new skolem expr
        //System.out.println("putting " + varId);
        _idToSkolemExpr.put(id_, skolemExpr);

        // create declaration for skolem function
        Variables vars = new Variables();
        vars.addVariable(skolemVar);

        MultiplicityExpr newMultExpr = ImplicitConstraintGenerator.createDesugaredMultExpr(setPrefix_, multExpr_);
        Decl skolemDecl = new Decl(new Qualifiers(), vars, newMultExpr);
        _leafIdToMult.put(skolemId, newMultExpr.copy());
       
        return _genConstraintsForSkolemFunction(skolemFunction, newMultExpr, multExpr_, skolemExpr);
    }

    /**
       create the set membership and multiplicity constraints for a skolem function
    */
    private Formula[] _genConstraintsForSkolemFunction(Expr skolemFunction_,
                                                       MultiplicityExpr multExpr_,
                                                       MultiplicityExpr origMultExpr_,
                                                       Expr skolemExpr_) {
        Formula[] ret = new Formula[2];
        Formulas constraints = new Formulas();
        Expr curExpr = skolemFunction_;
        Expr vExprSet = null;
        UnionType curType = multExpr_.getType();
        
        ElemFormula elemForm;
        // iterate through columns corresponding to universal quantifiers (if any)
        Iterator univVarIter = _univVarExprs.iterator();
        while (univVarIter.hasNext()) {
            VariableExpr vExpr = (VariableExpr)univVarIter.next();
            UnionType vType = vExpr.getType();
            UnionType oldType = curType;
            
            curType = vType.join(curType);
            vExprSet = (Expr)_varExprToSet.get(vExpr);
            Expr setExpr = new BinaryExpr((Expr)vExprSet.copy(),
                                          BinaryExprOp.RELATION,
                                          curType.toExpr());
            setExpr.setType(oldType);
            elemForm = new ElemFormula(curExpr,
                                       CompOp.SUBSETIN,
                                       setExpr);
            elemForm.annotate("set membership constraint");
            constraints.addFormula(elemForm);
            curExpr = new BinaryExpr((Expr)vExpr.copy(),
                                     BinaryExprOp.JOIN_DOT,
                                     (Expr)curExpr.copy());
            curExpr.setType(curType);
        }

        // now, handle relation types of original quantified variable being skolemized
        Expr origSetExpr = origMultExpr_.toExpr();
        // sanity check
        /** EMINA:  THIS CHECK IS TOO STRONG **/
        //Dbg.chk(curType.intersect(origSetExpr.getType()).equals(curType), origSetExpr.getType().toString() + " does not match " + curType.toString());
        elemForm = new ElemFormula(curExpr,
                                   CompOp.SUBSETIN,
                                   origSetExpr);
        elemForm.annotate("set membership constraint");
        constraints.addFormula(elemForm);

        Formula setMembConstraints = new FormulaSeq(constraints);
        setMembConstraints.annotate("constraints for skolem function " + skolemFunction_.nodeString());
        ret[0] = setMembConstraints;
        // handle multiplicities
	Formula multConstraint = new MultiplicityFormula((Expr)skolemExpr_.copy(), 
							 (MultiplicityExpr) origMultExpr_.copy());
	multConstraint = (Formula) multConstraint.applyReturnVisitor(new DesugarMultFormulasVisitor());
	multConstraint = (Formula) multConstraint.applyReturnVisitor(new DesugarQuantifiersVisitor());

	ret[1] = multConstraint;
	/**
        ret[1] = ImplicitConstraintGenerator.genMultiplicityConstraint(origMultExpr_, skolemExpr_);
	**/

        return ret;
    }

    /**
       create an expression which will replaces appearances of a quantified variable
       that has been skolemized
    */
    private Expr _createSkolemExpr(Expr skolemFunction_) {
        Expr skolemExpr = (Expr) skolemFunction_.copy();
        UnionType skolemExprType = skolemExpr.getType();

        Iterator univVarIter = _univVarExprs.iterator();
        while (univVarIter.hasNext()) {
            VariableExpr univVarExpr = (VariableExpr) univVarIter.next();
            // for vars x1, x2, ..., xn, skolem expr should be
            // xn.xn-1. ... .x2.x1.skolemFunction
            //RelationType rightType = skolemExpr.getType();
            //System.out.println(rightType);
            skolemExpr =
                new BinaryExpr((Expr) univVarExpr,
                               BinaryExprOp.JOIN_DOT,
                               skolemExpr);
            skolemExprType = univVarExpr.getType().join(skolemExprType);
            skolemExpr.setType(skolemExprType);
        }

        return skolemExpr;
    }

    /**
       create a set prefix expression for skolem constants based
       on the current universally quantified variables
    */
    private Expr _createSkolemSetPrefix() {
        Expr skolemSetPrefix = null;
        UnionType skolemTypePrefix = null;
        Iterator univVarIter = _univVarExprs.iterator();

        while (univVarIter.hasNext()) {
            VariableExpr univVarExpr = (VariableExpr) univVarIter.next();
            // for vars x1, x2, ..., xn with types t1, t2, ..., tn,
            // skolemTypePrefix should be t1 -> t2 -> ... -> tn and
        if (skolemTypePrefix == null)
        skolemTypePrefix = univVarExpr.getType();
        else
        skolemTypePrefix = skolemTypePrefix.product(univVarExpr.getType());
            Expr setExpr = (Expr)_varExprToSet.get(univVarExpr);
            Dbg.chk(setExpr);
            if (skolemSetPrefix == null) {
                skolemSetPrefix = setExpr;
                Dbg.chk(skolemSetPrefix.getType());
            } else {
                skolemSetPrefix = new BinaryExpr(skolemSetPrefix,
                                                 BinaryExprOp.RELATION,
                                                 setExpr);
                skolemSetPrefix.setType(skolemTypePrefix);
            }
        }

        return skolemSetPrefix;
    }

}
